i1, i2, j1, j2:. (i1  j1)  (i2  j2)  ((i1+i2)  (j1+j2)) 

latex

Up	int 2, int 2
Definitions	t  T, P  Q, x:A. B(x), False, A, A  B,
Lemmas	le wf